|
In mathematical logic, Craig's interpolation theorem is a result about the relationship between different logical theories. Roughly stated, the theorem says that if a formula φ implies a formula ψ, and the two have at least one atomic variable symbol in common, then there is a third formula ρ, called an interpolant, such that every nonlogical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ. The theorem was first proved for first-order logic by William Craig in 1957. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's theorem for first-order logic was proved by Roger Lyndon in 1959; the overall result is sometimes called the Craig–Lyndon theorem. == Example == In propositional logic, let :φ = ~(P ∧ Q) → (~R ∧ Q) :ψ = (T → P) ∨ (T → ~R). Then φ tautologically implies ψ. This can be verified by writing φ in conjunctive normal form: :φ ≡ (P ∨ ~R) ∧ Q. Thus, if φ holds, then (P ∨ ~R) holds. In turn, (P ∨ ~R) tautologically implies ψ. Because the two propositional variables occurring in (P ∨ ~R) occur in both φ and ψ, this means that (P ∨ ~R) is an interpolant for the implication φ → ψ. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Craig interpolation」の詳細全文を読む スポンサード リンク
|